(declare-fun z () Int)
(declare-fun b () (Seq Int))
(declare-fun y () Int)
(declare-fun a () (Seq Int))
(declare-fun x () Int)
(assert (and (= 1 z) (distinct (seq.nth b x) (seq.nth a z)) (= (seq.nth b y) (seq.nth b 1))))
(assert (> x 0))
(assert (> z 0))
(check-sat)
